mutation-trace protocol - #238

Establish the pure, dependency-free Rust domain layer that refines the verified mutation-cursor protocol. Register the new module with opaque identity types, boundary accessors, focused tests, and context documentation while leaving transition logic and production I/O integration for later plan tasks.

Plan: mutation-cursor-protocol-kernel (T01)

Co-authored-by: SCE <sce@crocoder.dev>

Prevent callers from pairing a hook boundary with unrelated scope state by resolving its worktree through the boundary's ScopeId in a scope map. Update regression tests and protocol documentation to capture the keyed lookup and correction.

Plan: mutation-cursor-protocol-kernel T01

Co-authored-by: SCE <sce@crocoder.dev>

Add the pure mutation-trace protocol kernel's aggregate state and prepare/commit evaluation for Start, Advance, Close, and Flush boundaries, including CAS freshness, replay, taint guards, scope lifecycle, cursor/revision, and attempt state transitions. Update the mutation-trace plan and repository context to record T02 completion and the explicit observation-input design. This keeps the kernel dependency-free while leaving attribution, event materialization, and recovery for follow-up tasks.

Plan: mutation-cursor-protocol-kernel (T02)

Co-authored-by: SCE <sce@crocoder.dev>

Refine the verified mutation-cursor protocol with pre-transition live-scope attribution and emit one MutationEvent for each accepted real tree change. Preserve Start and Close lifecycle semantics by evaluating evidence against the pre-transition state.

Plan: mutation-cursor-protocol-kernel, task T03

Co-authored-by: SCE <sce@crocoder.dev>

mod.rs and protocol.rs's module-level rustdoc still described
attribution derivation and mutation-event materialization as not yet
implemented, and protocol.rs's refinement list omitted liveScopesOn/
attributionFor/mkMutationEvent. Update both to describe the current
module state; only taint/database-failure/abandon/recovery remain
unimplemented. Documentation only, no behavior change.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W5m3Y3Jr9eW4iof3urzeMB

Co-authored-by: SCE <sce@crocoder.dev>

Model snapshot and database failures as guarded pure protocol transitions,
advancing snapshot-failure revisions and recording external taint without
changing unrelated worktree, scope, or mutation state.

Plan: mutation-cursor-protocol-kernel (T04)

Co-authored-by: SCE <sce@crocoder.dev>

Quint's WorktreeId ranges over the finite WORKTREES universe, and init
materializes a WorktreeState for every member, so recordDatabaseFailure has
no explicit worktree-existence guard because every WorktreeId already
resolves there. That omission described a fact about Quint's closed domain,
not license for the same gap in the unbounded Rust refinement.

database_failure previously had no existence guard, so an unknown
WorktreeId could be inserted into external_taint with no corresponding
ProtocolState.worktrees entry -- a state Quint cannot represent. Add the
same worktrees.contains_key guard taint already had, keeping
external_taint subset-of ProtocolState.worktrees an invariant of every
state this module can produce.

Add unknown-worktree no-op tests for both taint and database_failure.
Document the runtime worktree materialization contract (mirroring the
existing runtime scope materialization section) in the domain context
file, correct the plan's T04 result text, note the same existence
precondition on T05/T06's abandon/recover, and fix mod.rs's stale
"not yet implemented" doc comment for taint/database-failure.

No production call site references this module; spec/mutation_cursor.qnt
and spec/mutation_cursor.md are untouched.

Co-authored-by: SCE <sce@crocoder.dev>

Add the pure `abandon` transition that refines the verified mutation-cursor protocol for live scopes, preserving scope identity and cursor state while marking the owning worktree for rebaseline. Guard terminal, externally tainted, unknown, and unmaterialized states as no-ops, with focused Rust coverage.

Document the implemented protocol slice and cite the completed mutation-cursor-protocol-kernel plan task T05.

Co-authored-by: SCE <sce@crocoder.dev>

Add the pure recovery transition to complete the mutation-trace protocol action set. Rebaseline the cursor from an explicit observed tree, clear failure state and external taint, and abandon live scopes after taint recovery while preserving scopes for needs-rebaseline-only recovery.

Add focused recovery tests and synchronize the protocol context and plan records. Plan: mutation-cursor-protocol-kernel (T06)

Co-authored-by: SCE <sce@crocoder.dev>

…d revision overflow

PR review of T07 found three defects in the module's refinement matrix and one
unbounded-integer refinement gap:

- `AbandonCreatesRebaselineRequirement`, `MutationEventsMatchCursorHistory`, and
  `MutationEventsCrossOnlyTrustworthyProtocolStates` were classified
  verification-only because Quint states them via history/checkpoint variables,
  conflating the proof mechanism (verification-only) with the property it
  proves (production-semantic). Moved into the semantic-properties table, with
  a new regression test,
  `needs_rebaseline_suppresses_mutation_event_even_when_commit_observes_a_real_tree_change`,
  backing the third (no existing test drove `commit` through
  `accepted && observes && observed_change` against a `needs_rebaseline`
  worktree to prove `changed` still comes out false).
- `AiExclusiveRequiresExactlyOneActiveScope` was classified "enforced by Rust
  type", which is false: `Attribution::AiExclusive(ScopeId)` does not itself
  make an inconsistent scope count unrepresentable. Corrected to "implemented
  directly + preserved by transition tests", backed by `attribution_for`'s own
  `live.len() == 1` branch.
- Every revision-advancing action (`commit`, `taint`, `abandon`, `recover`)
  used a raw `worktree_state.revision + 1`, assuming a Rust `u64` can always
  refine Quint's unbounded `revision: int`. At `revision == u64::MAX` this
  would wrap to 0 in release mode.

Added a private `next_revision(revision: u64) -> Option<u64>` helper
(`checked_add(1)`) in `protocol.rs` and routed all four actions through it.
`commit`'s `accepted` gate folds in the headroom check unconditionally, before
`apply` touches any state, so an overflowing attempt is rejected exactly like a
stale one (no cursor movement, scope transition, processed-EventKey insertion,
or MutationEvent); `taint`/`abandon`/`recover` treat it as an additional
guarded no-op. Four new tests
(`commit_does_not_wrap_revision_at_u64_max`,
`taint_does_not_wrap_revision_at_u64_max`,
`abandon_does_not_wrap_revision_at_u64_max`,
`recover_does_not_wrap_revision_at_u64_max`) each start from
`revision: u64::MAX` and prove a no-op/rejection rather than a wrap.

Documented the refinement in a new `context/cli/mutation-trace-revision-refinement.md`
domain file, linked from `context/cli/mutation-trace-protocol.md` and
`context/context-map.md`.

74/74 mutation_trace tests pass (69 + 5 new); clippy and fmt clean;
spec/mutation_cursor.qnt is untouched and its own typecheck/test still pass.
No behavior changes to any previously-accepted transition.

mutation-cursor-protocol-kernel plan, T07 post-review correction.

Co-authored-by: SCE <sce@crocoder.dev>